$\forall$$T$:(Id$\rightarrow$Type), ${\it tab}$:secret{-}table($T$), $x$:Atom1.
\\[0ex]isl(st{-}lookup(${\it tab}$;$x$)) $\Leftrightarrow$ ($\exists$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$${\it tab}$$\parallel$ }}$. $n$$\leq$ptr(${\it tab}$) \& st{-}atom(${\it tab}$;$n$) $=$ $x$)